0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 85 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 4 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 197 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPSizeChangeProof (⇔, 0 ms)
↳43 YES
INTA_IN_GGA(0, s(X1), .(0, X2)) → U3_GGA(X1, X2, intA_in_gga(0, X1, X3))
INTA_IN_GGA(0, s(X1), .(0, X2)) → INTA_IN_GGA(0, X1, X3)
INTA_IN_GGA(0, s(X1), .(0, X2)) → U4_GGA(X1, X2, intcA_in_gga(0, X1, X3))
U4_GGA(X1, X2, intcA_out_gga(0, X1, X3)) → U5_GGA(X1, X2, intlistB_in_ga(X3, X2))
U4_GGA(X1, X2, intcA_out_gga(0, X1, X3)) → INTLISTB_IN_GA(X3, X2)
INTLISTB_IN_GA(.(X1, X2), .(s(X1), X3)) → U1_GA(X1, X2, X3, intlistB_in_ga(X2, X3))
INTLISTB_IN_GA(.(X1, X2), .(s(X1), X3)) → INTLISTB_IN_GA(X2, X3)
INTA_IN_GGA(s(0), s(s(X1)), X2) → U6_GGA(X1, X2, intA_in_gga(s(0), s(X1), X3))
INTA_IN_GGA(s(0), s(s(X1)), X2) → INTA_IN_GGA(s(0), s(X1), X3)
INTA_IN_GGA(s(0), s(s(X1)), X2) → U7_GGA(X1, X2, intcA_in_gga(s(0), s(X1), X3))
U7_GGA(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U8_GGA(X1, X2, intlistB_in_ga(.(0, X3), X2))
U7_GGA(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → INTLISTB_IN_GA(.(0, X3), X2)
INTA_IN_GGA(s(s(X1)), s(s(X2)), X3) → U9_GGA(X1, X2, X3, intA_in_gga(X1, X2, X4))
INTA_IN_GGA(s(s(X1)), s(s(X2)), X3) → INTA_IN_GGA(X1, X2, X4)
INTA_IN_GGA(s(s(X1)), s(s(X2)), X3) → U10_GGA(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U10_GGA(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U11_GGA(X1, X2, X3, intlistD_in_ga(X4, X5))
U10_GGA(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → INTLISTD_IN_GA(X4, X5)
INTLISTD_IN_GA(.(X1, X2), .(s(X1), X3)) → U2_GA(X1, X2, X3, intlistD_in_ga(X2, X3))
INTLISTD_IN_GA(.(X1, X2), .(s(X1), X3)) → INTLISTD_IN_GA(X2, X3)
U10_GGA(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U12_GGA(X1, X2, X3, intlistcD_in_ga(X4, X5))
U12_GGA(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U13_GGA(X1, X2, X3, intlistB_in_ga(X5, X3))
U12_GGA(X1, X2, X3, intlistcD_out_ga(X4, X5)) → INTLISTB_IN_GA(X5, X3)
intcA_in_gga(0, 0, .(0, [])) → intcA_out_gga(0, 0, .(0, []))
intcA_in_gga(0, s(X1), .(0, X2)) → U15_gga(X1, X2, intcA_in_gga(0, X1, X3))
intcA_in_gga(s(X1), 0, []) → intcA_out_gga(s(X1), 0, [])
intcA_in_gga(s(0), s(0), .(s(0), X1)) → U17_gga(X1, intlistcC_in_a(X1))
intlistcC_in_a([]) → intlistcC_out_a([])
U17_gga(X1, intlistcC_out_a(X1)) → intcA_out_gga(s(0), s(0), .(s(0), X1))
intcA_in_gga(s(0), s(s(X1)), X2) → U18_gga(X1, X2, intcA_in_gga(s(0), s(X1), X3))
intcA_in_gga(s(s(X1)), s(0), X2) → U20_gga(X1, X2, intlistcC_in_a(X2))
U20_gga(X1, X2, intlistcC_out_a(X2)) → intcA_out_gga(s(s(X1)), s(0), X2)
intcA_in_gga(s(s(X1)), s(s(X2)), X3) → U21_gga(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U21_gga(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U22_gga(X1, X2, X3, intlistcD_in_ga(X4, X5))
intlistcD_in_ga([], []) → intlistcD_out_ga([], [])
intlistcD_in_ga(.(X1, X2), .(s(X1), X3)) → U25_ga(X1, X2, X3, intlistcD_in_ga(X2, X3))
U25_ga(X1, X2, X3, intlistcD_out_ga(X2, X3)) → intlistcD_out_ga(.(X1, X2), .(s(X1), X3))
U22_gga(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U23_gga(X1, X2, X3, intlistcB_in_ga(X5, X3))
intlistcB_in_ga([], []) → intlistcB_out_ga([], [])
intlistcB_in_ga(.(X1, X2), .(s(X1), X3)) → U24_ga(X1, X2, X3, intlistcB_in_ga(X2, X3))
U24_ga(X1, X2, X3, intlistcB_out_ga(X2, X3)) → intlistcB_out_ga(.(X1, X2), .(s(X1), X3))
U23_gga(X1, X2, X3, intlistcB_out_ga(X5, X3)) → intcA_out_gga(s(s(X1)), s(s(X2)), X3)
U18_gga(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U19_gga(X1, X2, intlistcB_in_ga(.(0, X3), X2))
U19_gga(X1, X2, intlistcB_out_ga(.(0, X3), X2)) → intcA_out_gga(s(0), s(s(X1)), X2)
U15_gga(X1, X2, intcA_out_gga(0, X1, X3)) → U16_gga(X1, X2, intlistcB_in_ga(X3, X2))
U16_gga(X1, X2, intlistcB_out_ga(X3, X2)) → intcA_out_gga(0, s(X1), .(0, X2))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
INTA_IN_GGA(0, s(X1), .(0, X2)) → U3_GGA(X1, X2, intA_in_gga(0, X1, X3))
INTA_IN_GGA(0, s(X1), .(0, X2)) → INTA_IN_GGA(0, X1, X3)
INTA_IN_GGA(0, s(X1), .(0, X2)) → U4_GGA(X1, X2, intcA_in_gga(0, X1, X3))
U4_GGA(X1, X2, intcA_out_gga(0, X1, X3)) → U5_GGA(X1, X2, intlistB_in_ga(X3, X2))
U4_GGA(X1, X2, intcA_out_gga(0, X1, X3)) → INTLISTB_IN_GA(X3, X2)
INTLISTB_IN_GA(.(X1, X2), .(s(X1), X3)) → U1_GA(X1, X2, X3, intlistB_in_ga(X2, X3))
INTLISTB_IN_GA(.(X1, X2), .(s(X1), X3)) → INTLISTB_IN_GA(X2, X3)
INTA_IN_GGA(s(0), s(s(X1)), X2) → U6_GGA(X1, X2, intA_in_gga(s(0), s(X1), X3))
INTA_IN_GGA(s(0), s(s(X1)), X2) → INTA_IN_GGA(s(0), s(X1), X3)
INTA_IN_GGA(s(0), s(s(X1)), X2) → U7_GGA(X1, X2, intcA_in_gga(s(0), s(X1), X3))
U7_GGA(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U8_GGA(X1, X2, intlistB_in_ga(.(0, X3), X2))
U7_GGA(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → INTLISTB_IN_GA(.(0, X3), X2)
INTA_IN_GGA(s(s(X1)), s(s(X2)), X3) → U9_GGA(X1, X2, X3, intA_in_gga(X1, X2, X4))
INTA_IN_GGA(s(s(X1)), s(s(X2)), X3) → INTA_IN_GGA(X1, X2, X4)
INTA_IN_GGA(s(s(X1)), s(s(X2)), X3) → U10_GGA(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U10_GGA(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U11_GGA(X1, X2, X3, intlistD_in_ga(X4, X5))
U10_GGA(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → INTLISTD_IN_GA(X4, X5)
INTLISTD_IN_GA(.(X1, X2), .(s(X1), X3)) → U2_GA(X1, X2, X3, intlistD_in_ga(X2, X3))
INTLISTD_IN_GA(.(X1, X2), .(s(X1), X3)) → INTLISTD_IN_GA(X2, X3)
U10_GGA(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U12_GGA(X1, X2, X3, intlistcD_in_ga(X4, X5))
U12_GGA(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U13_GGA(X1, X2, X3, intlistB_in_ga(X5, X3))
U12_GGA(X1, X2, X3, intlistcD_out_ga(X4, X5)) → INTLISTB_IN_GA(X5, X3)
intcA_in_gga(0, 0, .(0, [])) → intcA_out_gga(0, 0, .(0, []))
intcA_in_gga(0, s(X1), .(0, X2)) → U15_gga(X1, X2, intcA_in_gga(0, X1, X3))
intcA_in_gga(s(X1), 0, []) → intcA_out_gga(s(X1), 0, [])
intcA_in_gga(s(0), s(0), .(s(0), X1)) → U17_gga(X1, intlistcC_in_a(X1))
intlistcC_in_a([]) → intlistcC_out_a([])
U17_gga(X1, intlistcC_out_a(X1)) → intcA_out_gga(s(0), s(0), .(s(0), X1))
intcA_in_gga(s(0), s(s(X1)), X2) → U18_gga(X1, X2, intcA_in_gga(s(0), s(X1), X3))
intcA_in_gga(s(s(X1)), s(0), X2) → U20_gga(X1, X2, intlistcC_in_a(X2))
U20_gga(X1, X2, intlistcC_out_a(X2)) → intcA_out_gga(s(s(X1)), s(0), X2)
intcA_in_gga(s(s(X1)), s(s(X2)), X3) → U21_gga(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U21_gga(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U22_gga(X1, X2, X3, intlistcD_in_ga(X4, X5))
intlistcD_in_ga([], []) → intlistcD_out_ga([], [])
intlistcD_in_ga(.(X1, X2), .(s(X1), X3)) → U25_ga(X1, X2, X3, intlistcD_in_ga(X2, X3))
U25_ga(X1, X2, X3, intlistcD_out_ga(X2, X3)) → intlistcD_out_ga(.(X1, X2), .(s(X1), X3))
U22_gga(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U23_gga(X1, X2, X3, intlistcB_in_ga(X5, X3))
intlistcB_in_ga([], []) → intlistcB_out_ga([], [])
intlistcB_in_ga(.(X1, X2), .(s(X1), X3)) → U24_ga(X1, X2, X3, intlistcB_in_ga(X2, X3))
U24_ga(X1, X2, X3, intlistcB_out_ga(X2, X3)) → intlistcB_out_ga(.(X1, X2), .(s(X1), X3))
U23_gga(X1, X2, X3, intlistcB_out_ga(X5, X3)) → intcA_out_gga(s(s(X1)), s(s(X2)), X3)
U18_gga(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U19_gga(X1, X2, intlistcB_in_ga(.(0, X3), X2))
U19_gga(X1, X2, intlistcB_out_ga(.(0, X3), X2)) → intcA_out_gga(s(0), s(s(X1)), X2)
U15_gga(X1, X2, intcA_out_gga(0, X1, X3)) → U16_gga(X1, X2, intlistcB_in_ga(X3, X2))
U16_gga(X1, X2, intlistcB_out_ga(X3, X2)) → intcA_out_gga(0, s(X1), .(0, X2))
INTLISTD_IN_GA(.(X1, X2), .(s(X1), X3)) → INTLISTD_IN_GA(X2, X3)
intcA_in_gga(0, 0, .(0, [])) → intcA_out_gga(0, 0, .(0, []))
intcA_in_gga(0, s(X1), .(0, X2)) → U15_gga(X1, X2, intcA_in_gga(0, X1, X3))
intcA_in_gga(s(X1), 0, []) → intcA_out_gga(s(X1), 0, [])
intcA_in_gga(s(0), s(0), .(s(0), X1)) → U17_gga(X1, intlistcC_in_a(X1))
intlistcC_in_a([]) → intlistcC_out_a([])
U17_gga(X1, intlistcC_out_a(X1)) → intcA_out_gga(s(0), s(0), .(s(0), X1))
intcA_in_gga(s(0), s(s(X1)), X2) → U18_gga(X1, X2, intcA_in_gga(s(0), s(X1), X3))
intcA_in_gga(s(s(X1)), s(0), X2) → U20_gga(X1, X2, intlistcC_in_a(X2))
U20_gga(X1, X2, intlistcC_out_a(X2)) → intcA_out_gga(s(s(X1)), s(0), X2)
intcA_in_gga(s(s(X1)), s(s(X2)), X3) → U21_gga(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U21_gga(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U22_gga(X1, X2, X3, intlistcD_in_ga(X4, X5))
intlistcD_in_ga([], []) → intlistcD_out_ga([], [])
intlistcD_in_ga(.(X1, X2), .(s(X1), X3)) → U25_ga(X1, X2, X3, intlistcD_in_ga(X2, X3))
U25_ga(X1, X2, X3, intlistcD_out_ga(X2, X3)) → intlistcD_out_ga(.(X1, X2), .(s(X1), X3))
U22_gga(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U23_gga(X1, X2, X3, intlistcB_in_ga(X5, X3))
intlistcB_in_ga([], []) → intlistcB_out_ga([], [])
intlistcB_in_ga(.(X1, X2), .(s(X1), X3)) → U24_ga(X1, X2, X3, intlistcB_in_ga(X2, X3))
U24_ga(X1, X2, X3, intlistcB_out_ga(X2, X3)) → intlistcB_out_ga(.(X1, X2), .(s(X1), X3))
U23_gga(X1, X2, X3, intlistcB_out_ga(X5, X3)) → intcA_out_gga(s(s(X1)), s(s(X2)), X3)
U18_gga(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U19_gga(X1, X2, intlistcB_in_ga(.(0, X3), X2))
U19_gga(X1, X2, intlistcB_out_ga(.(0, X3), X2)) → intcA_out_gga(s(0), s(s(X1)), X2)
U15_gga(X1, X2, intcA_out_gga(0, X1, X3)) → U16_gga(X1, X2, intlistcB_in_ga(X3, X2))
U16_gga(X1, X2, intlistcB_out_ga(X3, X2)) → intcA_out_gga(0, s(X1), .(0, X2))
INTLISTD_IN_GA(.(X1, X2), .(s(X1), X3)) → INTLISTD_IN_GA(X2, X3)
INTLISTD_IN_GA(.(X1, X2)) → INTLISTD_IN_GA(X2)
From the DPs we obtained the following set of size-change graphs:
INTLISTB_IN_GA(.(X1, X2), .(s(X1), X3)) → INTLISTB_IN_GA(X2, X3)
intcA_in_gga(0, 0, .(0, [])) → intcA_out_gga(0, 0, .(0, []))
intcA_in_gga(0, s(X1), .(0, X2)) → U15_gga(X1, X2, intcA_in_gga(0, X1, X3))
intcA_in_gga(s(X1), 0, []) → intcA_out_gga(s(X1), 0, [])
intcA_in_gga(s(0), s(0), .(s(0), X1)) → U17_gga(X1, intlistcC_in_a(X1))
intlistcC_in_a([]) → intlistcC_out_a([])
U17_gga(X1, intlistcC_out_a(X1)) → intcA_out_gga(s(0), s(0), .(s(0), X1))
intcA_in_gga(s(0), s(s(X1)), X2) → U18_gga(X1, X2, intcA_in_gga(s(0), s(X1), X3))
intcA_in_gga(s(s(X1)), s(0), X2) → U20_gga(X1, X2, intlistcC_in_a(X2))
U20_gga(X1, X2, intlistcC_out_a(X2)) → intcA_out_gga(s(s(X1)), s(0), X2)
intcA_in_gga(s(s(X1)), s(s(X2)), X3) → U21_gga(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U21_gga(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U22_gga(X1, X2, X3, intlistcD_in_ga(X4, X5))
intlistcD_in_ga([], []) → intlistcD_out_ga([], [])
intlistcD_in_ga(.(X1, X2), .(s(X1), X3)) → U25_ga(X1, X2, X3, intlistcD_in_ga(X2, X3))
U25_ga(X1, X2, X3, intlistcD_out_ga(X2, X3)) → intlistcD_out_ga(.(X1, X2), .(s(X1), X3))
U22_gga(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U23_gga(X1, X2, X3, intlistcB_in_ga(X5, X3))
intlistcB_in_ga([], []) → intlistcB_out_ga([], [])
intlistcB_in_ga(.(X1, X2), .(s(X1), X3)) → U24_ga(X1, X2, X3, intlistcB_in_ga(X2, X3))
U24_ga(X1, X2, X3, intlistcB_out_ga(X2, X3)) → intlistcB_out_ga(.(X1, X2), .(s(X1), X3))
U23_gga(X1, X2, X3, intlistcB_out_ga(X5, X3)) → intcA_out_gga(s(s(X1)), s(s(X2)), X3)
U18_gga(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U19_gga(X1, X2, intlistcB_in_ga(.(0, X3), X2))
U19_gga(X1, X2, intlistcB_out_ga(.(0, X3), X2)) → intcA_out_gga(s(0), s(s(X1)), X2)
U15_gga(X1, X2, intcA_out_gga(0, X1, X3)) → U16_gga(X1, X2, intlistcB_in_ga(X3, X2))
U16_gga(X1, X2, intlistcB_out_ga(X3, X2)) → intcA_out_gga(0, s(X1), .(0, X2))
INTLISTB_IN_GA(.(X1, X2), .(s(X1), X3)) → INTLISTB_IN_GA(X2, X3)
INTLISTB_IN_GA(.(X1, X2)) → INTLISTB_IN_GA(X2)
From the DPs we obtained the following set of size-change graphs:
INTA_IN_GGA(s(0), s(s(X1)), X2) → INTA_IN_GGA(s(0), s(X1), X3)
intcA_in_gga(0, 0, .(0, [])) → intcA_out_gga(0, 0, .(0, []))
intcA_in_gga(0, s(X1), .(0, X2)) → U15_gga(X1, X2, intcA_in_gga(0, X1, X3))
intcA_in_gga(s(X1), 0, []) → intcA_out_gga(s(X1), 0, [])
intcA_in_gga(s(0), s(0), .(s(0), X1)) → U17_gga(X1, intlistcC_in_a(X1))
intlistcC_in_a([]) → intlistcC_out_a([])
U17_gga(X1, intlistcC_out_a(X1)) → intcA_out_gga(s(0), s(0), .(s(0), X1))
intcA_in_gga(s(0), s(s(X1)), X2) → U18_gga(X1, X2, intcA_in_gga(s(0), s(X1), X3))
intcA_in_gga(s(s(X1)), s(0), X2) → U20_gga(X1, X2, intlistcC_in_a(X2))
U20_gga(X1, X2, intlistcC_out_a(X2)) → intcA_out_gga(s(s(X1)), s(0), X2)
intcA_in_gga(s(s(X1)), s(s(X2)), X3) → U21_gga(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U21_gga(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U22_gga(X1, X2, X3, intlistcD_in_ga(X4, X5))
intlistcD_in_ga([], []) → intlistcD_out_ga([], [])
intlistcD_in_ga(.(X1, X2), .(s(X1), X3)) → U25_ga(X1, X2, X3, intlistcD_in_ga(X2, X3))
U25_ga(X1, X2, X3, intlistcD_out_ga(X2, X3)) → intlistcD_out_ga(.(X1, X2), .(s(X1), X3))
U22_gga(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U23_gga(X1, X2, X3, intlistcB_in_ga(X5, X3))
intlistcB_in_ga([], []) → intlistcB_out_ga([], [])
intlistcB_in_ga(.(X1, X2), .(s(X1), X3)) → U24_ga(X1, X2, X3, intlistcB_in_ga(X2, X3))
U24_ga(X1, X2, X3, intlistcB_out_ga(X2, X3)) → intlistcB_out_ga(.(X1, X2), .(s(X1), X3))
U23_gga(X1, X2, X3, intlistcB_out_ga(X5, X3)) → intcA_out_gga(s(s(X1)), s(s(X2)), X3)
U18_gga(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U19_gga(X1, X2, intlistcB_in_ga(.(0, X3), X2))
U19_gga(X1, X2, intlistcB_out_ga(.(0, X3), X2)) → intcA_out_gga(s(0), s(s(X1)), X2)
U15_gga(X1, X2, intcA_out_gga(0, X1, X3)) → U16_gga(X1, X2, intlistcB_in_ga(X3, X2))
U16_gga(X1, X2, intlistcB_out_ga(X3, X2)) → intcA_out_gga(0, s(X1), .(0, X2))
INTA_IN_GGA(s(0), s(s(X1)), X2) → INTA_IN_GGA(s(0), s(X1), X3)
INTA_IN_GGA(s(0), s(s(X1))) → INTA_IN_GGA(s(0), s(X1))
From the DPs we obtained the following set of size-change graphs:
INTA_IN_GGA(0, s(X1), .(0, X2)) → INTA_IN_GGA(0, X1, X3)
intcA_in_gga(0, 0, .(0, [])) → intcA_out_gga(0, 0, .(0, []))
intcA_in_gga(0, s(X1), .(0, X2)) → U15_gga(X1, X2, intcA_in_gga(0, X1, X3))
intcA_in_gga(s(X1), 0, []) → intcA_out_gga(s(X1), 0, [])
intcA_in_gga(s(0), s(0), .(s(0), X1)) → U17_gga(X1, intlistcC_in_a(X1))
intlistcC_in_a([]) → intlistcC_out_a([])
U17_gga(X1, intlistcC_out_a(X1)) → intcA_out_gga(s(0), s(0), .(s(0), X1))
intcA_in_gga(s(0), s(s(X1)), X2) → U18_gga(X1, X2, intcA_in_gga(s(0), s(X1), X3))
intcA_in_gga(s(s(X1)), s(0), X2) → U20_gga(X1, X2, intlistcC_in_a(X2))
U20_gga(X1, X2, intlistcC_out_a(X2)) → intcA_out_gga(s(s(X1)), s(0), X2)
intcA_in_gga(s(s(X1)), s(s(X2)), X3) → U21_gga(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U21_gga(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U22_gga(X1, X2, X3, intlistcD_in_ga(X4, X5))
intlistcD_in_ga([], []) → intlistcD_out_ga([], [])
intlistcD_in_ga(.(X1, X2), .(s(X1), X3)) → U25_ga(X1, X2, X3, intlistcD_in_ga(X2, X3))
U25_ga(X1, X2, X3, intlistcD_out_ga(X2, X3)) → intlistcD_out_ga(.(X1, X2), .(s(X1), X3))
U22_gga(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U23_gga(X1, X2, X3, intlistcB_in_ga(X5, X3))
intlistcB_in_ga([], []) → intlistcB_out_ga([], [])
intlistcB_in_ga(.(X1, X2), .(s(X1), X3)) → U24_ga(X1, X2, X3, intlistcB_in_ga(X2, X3))
U24_ga(X1, X2, X3, intlistcB_out_ga(X2, X3)) → intlistcB_out_ga(.(X1, X2), .(s(X1), X3))
U23_gga(X1, X2, X3, intlistcB_out_ga(X5, X3)) → intcA_out_gga(s(s(X1)), s(s(X2)), X3)
U18_gga(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U19_gga(X1, X2, intlistcB_in_ga(.(0, X3), X2))
U19_gga(X1, X2, intlistcB_out_ga(.(0, X3), X2)) → intcA_out_gga(s(0), s(s(X1)), X2)
U15_gga(X1, X2, intcA_out_gga(0, X1, X3)) → U16_gga(X1, X2, intlistcB_in_ga(X3, X2))
U16_gga(X1, X2, intlistcB_out_ga(X3, X2)) → intcA_out_gga(0, s(X1), .(0, X2))
INTA_IN_GGA(0, s(X1), .(0, X2)) → INTA_IN_GGA(0, X1, X3)
INTA_IN_GGA(0, s(X1)) → INTA_IN_GGA(0, X1)
From the DPs we obtained the following set of size-change graphs:
INTA_IN_GGA(s(s(X1)), s(s(X2)), X3) → INTA_IN_GGA(X1, X2, X4)
intcA_in_gga(0, 0, .(0, [])) → intcA_out_gga(0, 0, .(0, []))
intcA_in_gga(0, s(X1), .(0, X2)) → U15_gga(X1, X2, intcA_in_gga(0, X1, X3))
intcA_in_gga(s(X1), 0, []) → intcA_out_gga(s(X1), 0, [])
intcA_in_gga(s(0), s(0), .(s(0), X1)) → U17_gga(X1, intlistcC_in_a(X1))
intlistcC_in_a([]) → intlistcC_out_a([])
U17_gga(X1, intlistcC_out_a(X1)) → intcA_out_gga(s(0), s(0), .(s(0), X1))
intcA_in_gga(s(0), s(s(X1)), X2) → U18_gga(X1, X2, intcA_in_gga(s(0), s(X1), X3))
intcA_in_gga(s(s(X1)), s(0), X2) → U20_gga(X1, X2, intlistcC_in_a(X2))
U20_gga(X1, X2, intlistcC_out_a(X2)) → intcA_out_gga(s(s(X1)), s(0), X2)
intcA_in_gga(s(s(X1)), s(s(X2)), X3) → U21_gga(X1, X2, X3, intcA_in_gga(X1, X2, X4))
U21_gga(X1, X2, X3, intcA_out_gga(X1, X2, X4)) → U22_gga(X1, X2, X3, intlistcD_in_ga(X4, X5))
intlistcD_in_ga([], []) → intlistcD_out_ga([], [])
intlistcD_in_ga(.(X1, X2), .(s(X1), X3)) → U25_ga(X1, X2, X3, intlistcD_in_ga(X2, X3))
U25_ga(X1, X2, X3, intlistcD_out_ga(X2, X3)) → intlistcD_out_ga(.(X1, X2), .(s(X1), X3))
U22_gga(X1, X2, X3, intlistcD_out_ga(X4, X5)) → U23_gga(X1, X2, X3, intlistcB_in_ga(X5, X3))
intlistcB_in_ga([], []) → intlistcB_out_ga([], [])
intlistcB_in_ga(.(X1, X2), .(s(X1), X3)) → U24_ga(X1, X2, X3, intlistcB_in_ga(X2, X3))
U24_ga(X1, X2, X3, intlistcB_out_ga(X2, X3)) → intlistcB_out_ga(.(X1, X2), .(s(X1), X3))
U23_gga(X1, X2, X3, intlistcB_out_ga(X5, X3)) → intcA_out_gga(s(s(X1)), s(s(X2)), X3)
U18_gga(X1, X2, intcA_out_gga(s(0), s(X1), X3)) → U19_gga(X1, X2, intlistcB_in_ga(.(0, X3), X2))
U19_gga(X1, X2, intlistcB_out_ga(.(0, X3), X2)) → intcA_out_gga(s(0), s(s(X1)), X2)
U15_gga(X1, X2, intcA_out_gga(0, X1, X3)) → U16_gga(X1, X2, intlistcB_in_ga(X3, X2))
U16_gga(X1, X2, intlistcB_out_ga(X3, X2)) → intcA_out_gga(0, s(X1), .(0, X2))
INTA_IN_GGA(s(s(X1)), s(s(X2)), X3) → INTA_IN_GGA(X1, X2, X4)
INTA_IN_GGA(s(s(X1)), s(s(X2))) → INTA_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs: